(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
a__dbl(0) → 0
a__dbl(s(X)) → s(s(dbl(X)))
a__dbls(nil) → nil
a__dbls(cons(X, Y)) → cons(dbl(X), dbls(Y))
a__sel(0, cons(X, Y)) → mark(X)
a__sel(s(X), cons(Y, Z)) → a__sel(mark(X), mark(Z))
a__indx(nil, X) → nil
a__indx(cons(X, Y), Z) → cons(sel(X, Z), indx(Y, Z))
a__from(X) → cons(X, from(s(X)))
a__dbl1(0) → 01
a__dbl1(s(X)) → s1(s1(a__dbl1(mark(X))))
a__sel1(0, cons(X, Y)) → mark(X)
a__sel1(s(X), cons(Y, Z)) → a__sel1(mark(X), mark(Z))
a__quote(0) → 01
a__quote(s(X)) → s1(a__quote(mark(X)))
a__quote(dbl(X)) → a__dbl1(mark(X))
a__quote(sel(X, Y)) → a__sel1(mark(X), mark(Y))
mark(dbl(X)) → a__dbl(mark(X))
mark(dbls(X)) → a__dbls(mark(X))
mark(sel(X1, X2)) → a__sel(mark(X1), mark(X2))
mark(indx(X1, X2)) → a__indx(mark(X1), X2)
mark(from(X)) → a__from(X)
mark(dbl1(X)) → a__dbl1(mark(X))
mark(sel1(X1, X2)) → a__sel1(mark(X1), mark(X2))
mark(quote(X)) → a__quote(mark(X))
mark(0) → 0
mark(s(X)) → s(X)
mark(nil) → nil
mark(cons(X1, X2)) → cons(X1, X2)
mark(01) → 01
mark(s1(X)) → s1(mark(X))
a__dbl(X) → dbl(X)
a__dbls(X) → dbls(X)
a__sel(X1, X2) → sel(X1, X2)
a__indx(X1, X2) → indx(X1, X2)
a__from(X) → from(X)
a__dbl1(X) → dbl1(X)
a__sel1(X1, X2) → sel1(X1, X2)
a__quote(X) → quote(X)
Rewrite Strategy: FULL
(1) DecreasingLoopProof (EQUIVALENT transformation)
The following loop(s) give(s) rise to the lower bound Ω(n1):
The rewrite sequence
a__sel(s(s(X1652_3)), cons(Y, cons(X13613_3, X23614_3))) →+ a__sel(s(X1652_3), cons(X13613_3, X23614_3))
gives rise to a decreasing loop by considering the right hand sides subterm at position [].
The pumping substitution is [X1652_3 / s(X1652_3), X23614_3 / cons(X13613_3, X23614_3)].
The result substitution is [Y / X13613_3].
(2) BOUNDS(n^1, INF)
(3) RenamingProof (EQUIVALENT transformation)
Renamed function symbols to avoid clashes with predefined symbol.
(4) Obligation:
Runtime Complexity Relative TRS:
The TRS R consists of the following rules:
a__dbl(0') → 0'
a__dbl(s(X)) → s(s(dbl(X)))
a__dbls(nil) → nil
a__dbls(cons(X, Y)) → cons(dbl(X), dbls(Y))
a__sel(0', cons(X, Y)) → mark(X)
a__sel(s(X), cons(Y, Z)) → a__sel(mark(X), mark(Z))
a__indx(nil, X) → nil
a__indx(cons(X, Y), Z) → cons(sel(X, Z), indx(Y, Z))
a__from(X) → cons(X, from(s(X)))
a__dbl1(0') → 01'
a__dbl1(s(X)) → s1(s1(a__dbl1(mark(X))))
a__sel1(0', cons(X, Y)) → mark(X)
a__sel1(s(X), cons(Y, Z)) → a__sel1(mark(X), mark(Z))
a__quote(0') → 01'
a__quote(s(X)) → s1(a__quote(mark(X)))
a__quote(dbl(X)) → a__dbl1(mark(X))
a__quote(sel(X, Y)) → a__sel1(mark(X), mark(Y))
mark(dbl(X)) → a__dbl(mark(X))
mark(dbls(X)) → a__dbls(mark(X))
mark(sel(X1, X2)) → a__sel(mark(X1), mark(X2))
mark(indx(X1, X2)) → a__indx(mark(X1), X2)
mark(from(X)) → a__from(X)
mark(dbl1(X)) → a__dbl1(mark(X))
mark(sel1(X1, X2)) → a__sel1(mark(X1), mark(X2))
mark(quote(X)) → a__quote(mark(X))
mark(0') → 0'
mark(s(X)) → s(X)
mark(nil) → nil
mark(cons(X1, X2)) → cons(X1, X2)
mark(01') → 01'
mark(s1(X)) → s1(mark(X))
a__dbl(X) → dbl(X)
a__dbls(X) → dbls(X)
a__sel(X1, X2) → sel(X1, X2)
a__indx(X1, X2) → indx(X1, X2)
a__from(X) → from(X)
a__dbl1(X) → dbl1(X)
a__sel1(X1, X2) → sel1(X1, X2)
a__quote(X) → quote(X)
S is empty.
Rewrite Strategy: FULL
(5) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)
Infered types.
(6) Obligation:
TRS:
Rules:
a__dbl(0') → 0'
a__dbl(s(X)) → s(s(dbl(X)))
a__dbls(nil) → nil
a__dbls(cons(X, Y)) → cons(dbl(X), dbls(Y))
a__sel(0', cons(X, Y)) → mark(X)
a__sel(s(X), cons(Y, Z)) → a__sel(mark(X), mark(Z))
a__indx(nil, X) → nil
a__indx(cons(X, Y), Z) → cons(sel(X, Z), indx(Y, Z))
a__from(X) → cons(X, from(s(X)))
a__dbl1(0') → 01'
a__dbl1(s(X)) → s1(s1(a__dbl1(mark(X))))
a__sel1(0', cons(X, Y)) → mark(X)
a__sel1(s(X), cons(Y, Z)) → a__sel1(mark(X), mark(Z))
a__quote(0') → 01'
a__quote(s(X)) → s1(a__quote(mark(X)))
a__quote(dbl(X)) → a__dbl1(mark(X))
a__quote(sel(X, Y)) → a__sel1(mark(X), mark(Y))
mark(dbl(X)) → a__dbl(mark(X))
mark(dbls(X)) → a__dbls(mark(X))
mark(sel(X1, X2)) → a__sel(mark(X1), mark(X2))
mark(indx(X1, X2)) → a__indx(mark(X1), X2)
mark(from(X)) → a__from(X)
mark(dbl1(X)) → a__dbl1(mark(X))
mark(sel1(X1, X2)) → a__sel1(mark(X1), mark(X2))
mark(quote(X)) → a__quote(mark(X))
mark(0') → 0'
mark(s(X)) → s(X)
mark(nil) → nil
mark(cons(X1, X2)) → cons(X1, X2)
mark(01') → 01'
mark(s1(X)) → s1(mark(X))
a__dbl(X) → dbl(X)
a__dbls(X) → dbls(X)
a__sel(X1, X2) → sel(X1, X2)
a__indx(X1, X2) → indx(X1, X2)
a__from(X) → from(X)
a__dbl1(X) → dbl1(X)
a__sel1(X1, X2) → sel1(X1, X2)
a__quote(X) → quote(X)
Types:
a__dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
0' :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
s :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
nil :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
cons :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
mark :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__from :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
from :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__dbl1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
01' :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
s1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__sel1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__quote :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbl1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
sel1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
quote :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
hole_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote1_0 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0 :: Nat → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
(7) OrderProof (LOWER BOUND(ID) transformation)
Heuristically decided to analyse the following defined symbols:
a__sel,
mark,
a__dbl1,
a__sel1,
a__quoteThey will be analysed ascendingly in the following order:
a__sel = mark
a__sel = a__dbl1
a__sel = a__sel1
a__sel = a__quote
mark = a__dbl1
mark = a__sel1
mark = a__quote
a__dbl1 = a__sel1
a__dbl1 = a__quote
a__sel1 = a__quote
(8) Obligation:
TRS:
Rules:
a__dbl(
0') →
0'a__dbl(
s(
X)) →
s(
s(
dbl(
X)))
a__dbls(
nil) →
nila__dbls(
cons(
X,
Y)) →
cons(
dbl(
X),
dbls(
Y))
a__sel(
0',
cons(
X,
Y)) →
mark(
X)
a__sel(
s(
X),
cons(
Y,
Z)) →
a__sel(
mark(
X),
mark(
Z))
a__indx(
nil,
X) →
nila__indx(
cons(
X,
Y),
Z) →
cons(
sel(
X,
Z),
indx(
Y,
Z))
a__from(
X) →
cons(
X,
from(
s(
X)))
a__dbl1(
0') →
01'a__dbl1(
s(
X)) →
s1(
s1(
a__dbl1(
mark(
X))))
a__sel1(
0',
cons(
X,
Y)) →
mark(
X)
a__sel1(
s(
X),
cons(
Y,
Z)) →
a__sel1(
mark(
X),
mark(
Z))
a__quote(
0') →
01'a__quote(
s(
X)) →
s1(
a__quote(
mark(
X)))
a__quote(
dbl(
X)) →
a__dbl1(
mark(
X))
a__quote(
sel(
X,
Y)) →
a__sel1(
mark(
X),
mark(
Y))
mark(
dbl(
X)) →
a__dbl(
mark(
X))
mark(
dbls(
X)) →
a__dbls(
mark(
X))
mark(
sel(
X1,
X2)) →
a__sel(
mark(
X1),
mark(
X2))
mark(
indx(
X1,
X2)) →
a__indx(
mark(
X1),
X2)
mark(
from(
X)) →
a__from(
X)
mark(
dbl1(
X)) →
a__dbl1(
mark(
X))
mark(
sel1(
X1,
X2)) →
a__sel1(
mark(
X1),
mark(
X2))
mark(
quote(
X)) →
a__quote(
mark(
X))
mark(
0') →
0'mark(
s(
X)) →
s(
X)
mark(
nil) →
nilmark(
cons(
X1,
X2)) →
cons(
X1,
X2)
mark(
01') →
01'mark(
s1(
X)) →
s1(
mark(
X))
a__dbl(
X) →
dbl(
X)
a__dbls(
X) →
dbls(
X)
a__sel(
X1,
X2) →
sel(
X1,
X2)
a__indx(
X1,
X2) →
indx(
X1,
X2)
a__from(
X) →
from(
X)
a__dbl1(
X) →
dbl1(
X)
a__sel1(
X1,
X2) →
sel1(
X1,
X2)
a__quote(
X) →
quote(
X)
Types:
a__dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
0' :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
s :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
nil :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
cons :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
mark :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__from :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
from :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__dbl1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
01' :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
s1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__sel1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__quote :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbl1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
sel1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
quote :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
hole_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote1_0 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0 :: Nat → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
Generator Equations:
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(0) ⇔ 0'
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(x, 1)) ⇔ s(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(x))
The following defined symbols remain to be analysed:
mark, a__sel, a__dbl1, a__sel1, a__quote
They will be analysed ascendingly in the following order:
a__sel = mark
a__sel = a__dbl1
a__sel = a__sel1
a__sel = a__quote
mark = a__dbl1
mark = a__sel1
mark = a__quote
a__dbl1 = a__sel1
a__dbl1 = a__quote
a__sel1 = a__quote
(9) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol mark.
(10) Obligation:
TRS:
Rules:
a__dbl(
0') →
0'a__dbl(
s(
X)) →
s(
s(
dbl(
X)))
a__dbls(
nil) →
nila__dbls(
cons(
X,
Y)) →
cons(
dbl(
X),
dbls(
Y))
a__sel(
0',
cons(
X,
Y)) →
mark(
X)
a__sel(
s(
X),
cons(
Y,
Z)) →
a__sel(
mark(
X),
mark(
Z))
a__indx(
nil,
X) →
nila__indx(
cons(
X,
Y),
Z) →
cons(
sel(
X,
Z),
indx(
Y,
Z))
a__from(
X) →
cons(
X,
from(
s(
X)))
a__dbl1(
0') →
01'a__dbl1(
s(
X)) →
s1(
s1(
a__dbl1(
mark(
X))))
a__sel1(
0',
cons(
X,
Y)) →
mark(
X)
a__sel1(
s(
X),
cons(
Y,
Z)) →
a__sel1(
mark(
X),
mark(
Z))
a__quote(
0') →
01'a__quote(
s(
X)) →
s1(
a__quote(
mark(
X)))
a__quote(
dbl(
X)) →
a__dbl1(
mark(
X))
a__quote(
sel(
X,
Y)) →
a__sel1(
mark(
X),
mark(
Y))
mark(
dbl(
X)) →
a__dbl(
mark(
X))
mark(
dbls(
X)) →
a__dbls(
mark(
X))
mark(
sel(
X1,
X2)) →
a__sel(
mark(
X1),
mark(
X2))
mark(
indx(
X1,
X2)) →
a__indx(
mark(
X1),
X2)
mark(
from(
X)) →
a__from(
X)
mark(
dbl1(
X)) →
a__dbl1(
mark(
X))
mark(
sel1(
X1,
X2)) →
a__sel1(
mark(
X1),
mark(
X2))
mark(
quote(
X)) →
a__quote(
mark(
X))
mark(
0') →
0'mark(
s(
X)) →
s(
X)
mark(
nil) →
nilmark(
cons(
X1,
X2)) →
cons(
X1,
X2)
mark(
01') →
01'mark(
s1(
X)) →
s1(
mark(
X))
a__dbl(
X) →
dbl(
X)
a__dbls(
X) →
dbls(
X)
a__sel(
X1,
X2) →
sel(
X1,
X2)
a__indx(
X1,
X2) →
indx(
X1,
X2)
a__from(
X) →
from(
X)
a__dbl1(
X) →
dbl1(
X)
a__sel1(
X1,
X2) →
sel1(
X1,
X2)
a__quote(
X) →
quote(
X)
Types:
a__dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
0' :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
s :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
nil :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
cons :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
mark :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__from :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
from :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__dbl1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
01' :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
s1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__sel1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__quote :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbl1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
sel1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
quote :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
hole_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote1_0 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0 :: Nat → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
Generator Equations:
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(0) ⇔ 0'
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(x, 1)) ⇔ s(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(x))
The following defined symbols remain to be analysed:
a__sel, a__dbl1, a__sel1, a__quote
They will be analysed ascendingly in the following order:
a__sel = mark
a__sel = a__dbl1
a__sel = a__sel1
a__sel = a__quote
mark = a__dbl1
mark = a__sel1
mark = a__quote
a__dbl1 = a__sel1
a__dbl1 = a__quote
a__sel1 = a__quote
(11) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol a__sel.
(12) Obligation:
TRS:
Rules:
a__dbl(
0') →
0'a__dbl(
s(
X)) →
s(
s(
dbl(
X)))
a__dbls(
nil) →
nila__dbls(
cons(
X,
Y)) →
cons(
dbl(
X),
dbls(
Y))
a__sel(
0',
cons(
X,
Y)) →
mark(
X)
a__sel(
s(
X),
cons(
Y,
Z)) →
a__sel(
mark(
X),
mark(
Z))
a__indx(
nil,
X) →
nila__indx(
cons(
X,
Y),
Z) →
cons(
sel(
X,
Z),
indx(
Y,
Z))
a__from(
X) →
cons(
X,
from(
s(
X)))
a__dbl1(
0') →
01'a__dbl1(
s(
X)) →
s1(
s1(
a__dbl1(
mark(
X))))
a__sel1(
0',
cons(
X,
Y)) →
mark(
X)
a__sel1(
s(
X),
cons(
Y,
Z)) →
a__sel1(
mark(
X),
mark(
Z))
a__quote(
0') →
01'a__quote(
s(
X)) →
s1(
a__quote(
mark(
X)))
a__quote(
dbl(
X)) →
a__dbl1(
mark(
X))
a__quote(
sel(
X,
Y)) →
a__sel1(
mark(
X),
mark(
Y))
mark(
dbl(
X)) →
a__dbl(
mark(
X))
mark(
dbls(
X)) →
a__dbls(
mark(
X))
mark(
sel(
X1,
X2)) →
a__sel(
mark(
X1),
mark(
X2))
mark(
indx(
X1,
X2)) →
a__indx(
mark(
X1),
X2)
mark(
from(
X)) →
a__from(
X)
mark(
dbl1(
X)) →
a__dbl1(
mark(
X))
mark(
sel1(
X1,
X2)) →
a__sel1(
mark(
X1),
mark(
X2))
mark(
quote(
X)) →
a__quote(
mark(
X))
mark(
0') →
0'mark(
s(
X)) →
s(
X)
mark(
nil) →
nilmark(
cons(
X1,
X2)) →
cons(
X1,
X2)
mark(
01') →
01'mark(
s1(
X)) →
s1(
mark(
X))
a__dbl(
X) →
dbl(
X)
a__dbls(
X) →
dbls(
X)
a__sel(
X1,
X2) →
sel(
X1,
X2)
a__indx(
X1,
X2) →
indx(
X1,
X2)
a__from(
X) →
from(
X)
a__dbl1(
X) →
dbl1(
X)
a__sel1(
X1,
X2) →
sel1(
X1,
X2)
a__quote(
X) →
quote(
X)
Types:
a__dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
0' :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
s :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
nil :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
cons :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
mark :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__from :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
from :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__dbl1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
01' :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
s1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__sel1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__quote :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbl1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
sel1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
quote :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
hole_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote1_0 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0 :: Nat → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
Generator Equations:
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(0) ⇔ 0'
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(x, 1)) ⇔ s(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(x))
The following defined symbols remain to be analysed:
a__dbl1, a__sel1, a__quote
They will be analysed ascendingly in the following order:
a__sel = mark
a__sel = a__dbl1
a__sel = a__sel1
a__sel = a__quote
mark = a__dbl1
mark = a__sel1
mark = a__quote
a__dbl1 = a__sel1
a__dbl1 = a__quote
a__sel1 = a__quote
(13) RewriteLemmaProof (LOWER BOUND(ID) transformation)
Proved the following rewrite lemma:
a__dbl1(
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(
+(
1,
n79116_0))) →
*3_0, rt ∈ Ω(n79116
0)
Induction Base:
a__dbl1(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, 0)))
Induction Step:
a__dbl1(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, +(n79116_0, 1)))) →RΩ(1)
s1(s1(a__dbl1(mark(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, n79116_0)))))) →RΩ(1)
s1(s1(a__dbl1(s(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(n79116_0))))) →IH
s1(s1(*3_0))
We have rt ∈ Ω(n1) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
(14) Complex Obligation (BEST)
(15) Obligation:
TRS:
Rules:
a__dbl(
0') →
0'a__dbl(
s(
X)) →
s(
s(
dbl(
X)))
a__dbls(
nil) →
nila__dbls(
cons(
X,
Y)) →
cons(
dbl(
X),
dbls(
Y))
a__sel(
0',
cons(
X,
Y)) →
mark(
X)
a__sel(
s(
X),
cons(
Y,
Z)) →
a__sel(
mark(
X),
mark(
Z))
a__indx(
nil,
X) →
nila__indx(
cons(
X,
Y),
Z) →
cons(
sel(
X,
Z),
indx(
Y,
Z))
a__from(
X) →
cons(
X,
from(
s(
X)))
a__dbl1(
0') →
01'a__dbl1(
s(
X)) →
s1(
s1(
a__dbl1(
mark(
X))))
a__sel1(
0',
cons(
X,
Y)) →
mark(
X)
a__sel1(
s(
X),
cons(
Y,
Z)) →
a__sel1(
mark(
X),
mark(
Z))
a__quote(
0') →
01'a__quote(
s(
X)) →
s1(
a__quote(
mark(
X)))
a__quote(
dbl(
X)) →
a__dbl1(
mark(
X))
a__quote(
sel(
X,
Y)) →
a__sel1(
mark(
X),
mark(
Y))
mark(
dbl(
X)) →
a__dbl(
mark(
X))
mark(
dbls(
X)) →
a__dbls(
mark(
X))
mark(
sel(
X1,
X2)) →
a__sel(
mark(
X1),
mark(
X2))
mark(
indx(
X1,
X2)) →
a__indx(
mark(
X1),
X2)
mark(
from(
X)) →
a__from(
X)
mark(
dbl1(
X)) →
a__dbl1(
mark(
X))
mark(
sel1(
X1,
X2)) →
a__sel1(
mark(
X1),
mark(
X2))
mark(
quote(
X)) →
a__quote(
mark(
X))
mark(
0') →
0'mark(
s(
X)) →
s(
X)
mark(
nil) →
nilmark(
cons(
X1,
X2)) →
cons(
X1,
X2)
mark(
01') →
01'mark(
s1(
X)) →
s1(
mark(
X))
a__dbl(
X) →
dbl(
X)
a__dbls(
X) →
dbls(
X)
a__sel(
X1,
X2) →
sel(
X1,
X2)
a__indx(
X1,
X2) →
indx(
X1,
X2)
a__from(
X) →
from(
X)
a__dbl1(
X) →
dbl1(
X)
a__sel1(
X1,
X2) →
sel1(
X1,
X2)
a__quote(
X) →
quote(
X)
Types:
a__dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
0' :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
s :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
nil :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
cons :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
mark :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__from :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
from :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__dbl1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
01' :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
s1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__sel1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__quote :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbl1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
sel1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
quote :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
hole_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote1_0 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0 :: Nat → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
Lemmas:
a__dbl1(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, n79116_0))) → *3_0, rt ∈ Ω(n791160)
Generator Equations:
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(0) ⇔ 0'
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(x, 1)) ⇔ s(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(x))
The following defined symbols remain to be analysed:
a__sel1, a__sel, mark, a__quote
They will be analysed ascendingly in the following order:
a__sel = mark
a__sel = a__dbl1
a__sel = a__sel1
a__sel = a__quote
mark = a__dbl1
mark = a__sel1
mark = a__quote
a__dbl1 = a__sel1
a__dbl1 = a__quote
a__sel1 = a__quote
(16) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol a__sel1.
(17) Obligation:
TRS:
Rules:
a__dbl(
0') →
0'a__dbl(
s(
X)) →
s(
s(
dbl(
X)))
a__dbls(
nil) →
nila__dbls(
cons(
X,
Y)) →
cons(
dbl(
X),
dbls(
Y))
a__sel(
0',
cons(
X,
Y)) →
mark(
X)
a__sel(
s(
X),
cons(
Y,
Z)) →
a__sel(
mark(
X),
mark(
Z))
a__indx(
nil,
X) →
nila__indx(
cons(
X,
Y),
Z) →
cons(
sel(
X,
Z),
indx(
Y,
Z))
a__from(
X) →
cons(
X,
from(
s(
X)))
a__dbl1(
0') →
01'a__dbl1(
s(
X)) →
s1(
s1(
a__dbl1(
mark(
X))))
a__sel1(
0',
cons(
X,
Y)) →
mark(
X)
a__sel1(
s(
X),
cons(
Y,
Z)) →
a__sel1(
mark(
X),
mark(
Z))
a__quote(
0') →
01'a__quote(
s(
X)) →
s1(
a__quote(
mark(
X)))
a__quote(
dbl(
X)) →
a__dbl1(
mark(
X))
a__quote(
sel(
X,
Y)) →
a__sel1(
mark(
X),
mark(
Y))
mark(
dbl(
X)) →
a__dbl(
mark(
X))
mark(
dbls(
X)) →
a__dbls(
mark(
X))
mark(
sel(
X1,
X2)) →
a__sel(
mark(
X1),
mark(
X2))
mark(
indx(
X1,
X2)) →
a__indx(
mark(
X1),
X2)
mark(
from(
X)) →
a__from(
X)
mark(
dbl1(
X)) →
a__dbl1(
mark(
X))
mark(
sel1(
X1,
X2)) →
a__sel1(
mark(
X1),
mark(
X2))
mark(
quote(
X)) →
a__quote(
mark(
X))
mark(
0') →
0'mark(
s(
X)) →
s(
X)
mark(
nil) →
nilmark(
cons(
X1,
X2)) →
cons(
X1,
X2)
mark(
01') →
01'mark(
s1(
X)) →
s1(
mark(
X))
a__dbl(
X) →
dbl(
X)
a__dbls(
X) →
dbls(
X)
a__sel(
X1,
X2) →
sel(
X1,
X2)
a__indx(
X1,
X2) →
indx(
X1,
X2)
a__from(
X) →
from(
X)
a__dbl1(
X) →
dbl1(
X)
a__sel1(
X1,
X2) →
sel1(
X1,
X2)
a__quote(
X) →
quote(
X)
Types:
a__dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
0' :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
s :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
nil :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
cons :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
mark :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__from :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
from :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__dbl1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
01' :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
s1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__sel1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__quote :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbl1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
sel1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
quote :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
hole_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote1_0 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0 :: Nat → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
Lemmas:
a__dbl1(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, n79116_0))) → *3_0, rt ∈ Ω(n791160)
Generator Equations:
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(0) ⇔ 0'
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(x, 1)) ⇔ s(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(x))
The following defined symbols remain to be analysed:
a__quote, a__sel, mark
They will be analysed ascendingly in the following order:
a__sel = mark
a__sel = a__dbl1
a__sel = a__sel1
a__sel = a__quote
mark = a__dbl1
mark = a__sel1
mark = a__quote
a__dbl1 = a__sel1
a__dbl1 = a__quote
a__sel1 = a__quote
(18) RewriteLemmaProof (LOWER BOUND(ID) transformation)
Proved the following rewrite lemma:
a__quote(
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(
+(
1,
n1977765_0))) →
*3_0, rt ∈ Ω(n1977765
0)
Induction Base:
a__quote(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, 0)))
Induction Step:
a__quote(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, +(n1977765_0, 1)))) →RΩ(1)
s1(a__quote(mark(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, n1977765_0))))) →RΩ(1)
s1(a__quote(s(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(n1977765_0)))) →IH
s1(*3_0)
We have rt ∈ Ω(n1) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
(19) Complex Obligation (BEST)
(20) Obligation:
TRS:
Rules:
a__dbl(
0') →
0'a__dbl(
s(
X)) →
s(
s(
dbl(
X)))
a__dbls(
nil) →
nila__dbls(
cons(
X,
Y)) →
cons(
dbl(
X),
dbls(
Y))
a__sel(
0',
cons(
X,
Y)) →
mark(
X)
a__sel(
s(
X),
cons(
Y,
Z)) →
a__sel(
mark(
X),
mark(
Z))
a__indx(
nil,
X) →
nila__indx(
cons(
X,
Y),
Z) →
cons(
sel(
X,
Z),
indx(
Y,
Z))
a__from(
X) →
cons(
X,
from(
s(
X)))
a__dbl1(
0') →
01'a__dbl1(
s(
X)) →
s1(
s1(
a__dbl1(
mark(
X))))
a__sel1(
0',
cons(
X,
Y)) →
mark(
X)
a__sel1(
s(
X),
cons(
Y,
Z)) →
a__sel1(
mark(
X),
mark(
Z))
a__quote(
0') →
01'a__quote(
s(
X)) →
s1(
a__quote(
mark(
X)))
a__quote(
dbl(
X)) →
a__dbl1(
mark(
X))
a__quote(
sel(
X,
Y)) →
a__sel1(
mark(
X),
mark(
Y))
mark(
dbl(
X)) →
a__dbl(
mark(
X))
mark(
dbls(
X)) →
a__dbls(
mark(
X))
mark(
sel(
X1,
X2)) →
a__sel(
mark(
X1),
mark(
X2))
mark(
indx(
X1,
X2)) →
a__indx(
mark(
X1),
X2)
mark(
from(
X)) →
a__from(
X)
mark(
dbl1(
X)) →
a__dbl1(
mark(
X))
mark(
sel1(
X1,
X2)) →
a__sel1(
mark(
X1),
mark(
X2))
mark(
quote(
X)) →
a__quote(
mark(
X))
mark(
0') →
0'mark(
s(
X)) →
s(
X)
mark(
nil) →
nilmark(
cons(
X1,
X2)) →
cons(
X1,
X2)
mark(
01') →
01'mark(
s1(
X)) →
s1(
mark(
X))
a__dbl(
X) →
dbl(
X)
a__dbls(
X) →
dbls(
X)
a__sel(
X1,
X2) →
sel(
X1,
X2)
a__indx(
X1,
X2) →
indx(
X1,
X2)
a__from(
X) →
from(
X)
a__dbl1(
X) →
dbl1(
X)
a__sel1(
X1,
X2) →
sel1(
X1,
X2)
a__quote(
X) →
quote(
X)
Types:
a__dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
0' :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
s :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
nil :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
cons :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
mark :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__from :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
from :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__dbl1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
01' :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
s1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__sel1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__quote :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbl1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
sel1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
quote :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
hole_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote1_0 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0 :: Nat → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
Lemmas:
a__dbl1(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, n79116_0))) → *3_0, rt ∈ Ω(n791160)
a__quote(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, n1977765_0))) → *3_0, rt ∈ Ω(n19777650)
Generator Equations:
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(0) ⇔ 0'
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(x, 1)) ⇔ s(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(x))
The following defined symbols remain to be analysed:
mark, a__sel, a__dbl1, a__sel1
They will be analysed ascendingly in the following order:
a__sel = mark
a__sel = a__dbl1
a__sel = a__sel1
a__sel = a__quote
mark = a__dbl1
mark = a__sel1
mark = a__quote
a__dbl1 = a__sel1
a__dbl1 = a__quote
a__sel1 = a__quote
(21) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol mark.
(22) Obligation:
TRS:
Rules:
a__dbl(
0') →
0'a__dbl(
s(
X)) →
s(
s(
dbl(
X)))
a__dbls(
nil) →
nila__dbls(
cons(
X,
Y)) →
cons(
dbl(
X),
dbls(
Y))
a__sel(
0',
cons(
X,
Y)) →
mark(
X)
a__sel(
s(
X),
cons(
Y,
Z)) →
a__sel(
mark(
X),
mark(
Z))
a__indx(
nil,
X) →
nila__indx(
cons(
X,
Y),
Z) →
cons(
sel(
X,
Z),
indx(
Y,
Z))
a__from(
X) →
cons(
X,
from(
s(
X)))
a__dbl1(
0') →
01'a__dbl1(
s(
X)) →
s1(
s1(
a__dbl1(
mark(
X))))
a__sel1(
0',
cons(
X,
Y)) →
mark(
X)
a__sel1(
s(
X),
cons(
Y,
Z)) →
a__sel1(
mark(
X),
mark(
Z))
a__quote(
0') →
01'a__quote(
s(
X)) →
s1(
a__quote(
mark(
X)))
a__quote(
dbl(
X)) →
a__dbl1(
mark(
X))
a__quote(
sel(
X,
Y)) →
a__sel1(
mark(
X),
mark(
Y))
mark(
dbl(
X)) →
a__dbl(
mark(
X))
mark(
dbls(
X)) →
a__dbls(
mark(
X))
mark(
sel(
X1,
X2)) →
a__sel(
mark(
X1),
mark(
X2))
mark(
indx(
X1,
X2)) →
a__indx(
mark(
X1),
X2)
mark(
from(
X)) →
a__from(
X)
mark(
dbl1(
X)) →
a__dbl1(
mark(
X))
mark(
sel1(
X1,
X2)) →
a__sel1(
mark(
X1),
mark(
X2))
mark(
quote(
X)) →
a__quote(
mark(
X))
mark(
0') →
0'mark(
s(
X)) →
s(
X)
mark(
nil) →
nilmark(
cons(
X1,
X2)) →
cons(
X1,
X2)
mark(
01') →
01'mark(
s1(
X)) →
s1(
mark(
X))
a__dbl(
X) →
dbl(
X)
a__dbls(
X) →
dbls(
X)
a__sel(
X1,
X2) →
sel(
X1,
X2)
a__indx(
X1,
X2) →
indx(
X1,
X2)
a__from(
X) →
from(
X)
a__dbl1(
X) →
dbl1(
X)
a__sel1(
X1,
X2) →
sel1(
X1,
X2)
a__quote(
X) →
quote(
X)
Types:
a__dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
0' :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
s :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
nil :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
cons :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
mark :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__from :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
from :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__dbl1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
01' :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
s1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__sel1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__quote :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbl1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
sel1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
quote :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
hole_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote1_0 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0 :: Nat → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
Lemmas:
a__dbl1(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, n79116_0))) → *3_0, rt ∈ Ω(n791160)
a__quote(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, n1977765_0))) → *3_0, rt ∈ Ω(n19777650)
Generator Equations:
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(0) ⇔ 0'
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(x, 1)) ⇔ s(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(x))
The following defined symbols remain to be analysed:
a__sel, a__dbl1, a__sel1
They will be analysed ascendingly in the following order:
a__sel = mark
a__sel = a__dbl1
a__sel = a__sel1
a__sel = a__quote
mark = a__dbl1
mark = a__sel1
mark = a__quote
a__dbl1 = a__sel1
a__dbl1 = a__quote
a__sel1 = a__quote
(23) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol a__sel.
(24) Obligation:
TRS:
Rules:
a__dbl(
0') →
0'a__dbl(
s(
X)) →
s(
s(
dbl(
X)))
a__dbls(
nil) →
nila__dbls(
cons(
X,
Y)) →
cons(
dbl(
X),
dbls(
Y))
a__sel(
0',
cons(
X,
Y)) →
mark(
X)
a__sel(
s(
X),
cons(
Y,
Z)) →
a__sel(
mark(
X),
mark(
Z))
a__indx(
nil,
X) →
nila__indx(
cons(
X,
Y),
Z) →
cons(
sel(
X,
Z),
indx(
Y,
Z))
a__from(
X) →
cons(
X,
from(
s(
X)))
a__dbl1(
0') →
01'a__dbl1(
s(
X)) →
s1(
s1(
a__dbl1(
mark(
X))))
a__sel1(
0',
cons(
X,
Y)) →
mark(
X)
a__sel1(
s(
X),
cons(
Y,
Z)) →
a__sel1(
mark(
X),
mark(
Z))
a__quote(
0') →
01'a__quote(
s(
X)) →
s1(
a__quote(
mark(
X)))
a__quote(
dbl(
X)) →
a__dbl1(
mark(
X))
a__quote(
sel(
X,
Y)) →
a__sel1(
mark(
X),
mark(
Y))
mark(
dbl(
X)) →
a__dbl(
mark(
X))
mark(
dbls(
X)) →
a__dbls(
mark(
X))
mark(
sel(
X1,
X2)) →
a__sel(
mark(
X1),
mark(
X2))
mark(
indx(
X1,
X2)) →
a__indx(
mark(
X1),
X2)
mark(
from(
X)) →
a__from(
X)
mark(
dbl1(
X)) →
a__dbl1(
mark(
X))
mark(
sel1(
X1,
X2)) →
a__sel1(
mark(
X1),
mark(
X2))
mark(
quote(
X)) →
a__quote(
mark(
X))
mark(
0') →
0'mark(
s(
X)) →
s(
X)
mark(
nil) →
nilmark(
cons(
X1,
X2)) →
cons(
X1,
X2)
mark(
01') →
01'mark(
s1(
X)) →
s1(
mark(
X))
a__dbl(
X) →
dbl(
X)
a__dbls(
X) →
dbls(
X)
a__sel(
X1,
X2) →
sel(
X1,
X2)
a__indx(
X1,
X2) →
indx(
X1,
X2)
a__from(
X) →
from(
X)
a__dbl1(
X) →
dbl1(
X)
a__sel1(
X1,
X2) →
sel1(
X1,
X2)
a__quote(
X) →
quote(
X)
Types:
a__dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
0' :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
s :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
nil :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
cons :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
mark :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__from :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
from :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__dbl1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
01' :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
s1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__sel1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__quote :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbl1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
sel1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
quote :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
hole_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote1_0 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0 :: Nat → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
Lemmas:
a__dbl1(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, n79116_0))) → *3_0, rt ∈ Ω(n791160)
a__quote(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, n1977765_0))) → *3_0, rt ∈ Ω(n19777650)
Generator Equations:
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(0) ⇔ 0'
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(x, 1)) ⇔ s(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(x))
The following defined symbols remain to be analysed:
a__dbl1, a__sel1
They will be analysed ascendingly in the following order:
a__sel = mark
a__sel = a__dbl1
a__sel = a__sel1
a__sel = a__quote
mark = a__dbl1
mark = a__sel1
mark = a__quote
a__dbl1 = a__sel1
a__dbl1 = a__quote
a__sel1 = a__quote
(25) RewriteLemmaProof (LOWER BOUND(ID) transformation)
Proved the following rewrite lemma:
a__dbl1(
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(
+(
1,
n3958080_0))) →
*3_0, rt ∈ Ω(n3958080
0)
Induction Base:
a__dbl1(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, 0)))
Induction Step:
a__dbl1(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, +(n3958080_0, 1)))) →RΩ(1)
s1(s1(a__dbl1(mark(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, n3958080_0)))))) →RΩ(1)
s1(s1(a__dbl1(s(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(n3958080_0))))) →IH
s1(s1(*3_0))
We have rt ∈ Ω(n1) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
(26) Complex Obligation (BEST)
(27) Obligation:
TRS:
Rules:
a__dbl(
0') →
0'a__dbl(
s(
X)) →
s(
s(
dbl(
X)))
a__dbls(
nil) →
nila__dbls(
cons(
X,
Y)) →
cons(
dbl(
X),
dbls(
Y))
a__sel(
0',
cons(
X,
Y)) →
mark(
X)
a__sel(
s(
X),
cons(
Y,
Z)) →
a__sel(
mark(
X),
mark(
Z))
a__indx(
nil,
X) →
nila__indx(
cons(
X,
Y),
Z) →
cons(
sel(
X,
Z),
indx(
Y,
Z))
a__from(
X) →
cons(
X,
from(
s(
X)))
a__dbl1(
0') →
01'a__dbl1(
s(
X)) →
s1(
s1(
a__dbl1(
mark(
X))))
a__sel1(
0',
cons(
X,
Y)) →
mark(
X)
a__sel1(
s(
X),
cons(
Y,
Z)) →
a__sel1(
mark(
X),
mark(
Z))
a__quote(
0') →
01'a__quote(
s(
X)) →
s1(
a__quote(
mark(
X)))
a__quote(
dbl(
X)) →
a__dbl1(
mark(
X))
a__quote(
sel(
X,
Y)) →
a__sel1(
mark(
X),
mark(
Y))
mark(
dbl(
X)) →
a__dbl(
mark(
X))
mark(
dbls(
X)) →
a__dbls(
mark(
X))
mark(
sel(
X1,
X2)) →
a__sel(
mark(
X1),
mark(
X2))
mark(
indx(
X1,
X2)) →
a__indx(
mark(
X1),
X2)
mark(
from(
X)) →
a__from(
X)
mark(
dbl1(
X)) →
a__dbl1(
mark(
X))
mark(
sel1(
X1,
X2)) →
a__sel1(
mark(
X1),
mark(
X2))
mark(
quote(
X)) →
a__quote(
mark(
X))
mark(
0') →
0'mark(
s(
X)) →
s(
X)
mark(
nil) →
nilmark(
cons(
X1,
X2)) →
cons(
X1,
X2)
mark(
01') →
01'mark(
s1(
X)) →
s1(
mark(
X))
a__dbl(
X) →
dbl(
X)
a__dbls(
X) →
dbls(
X)
a__sel(
X1,
X2) →
sel(
X1,
X2)
a__indx(
X1,
X2) →
indx(
X1,
X2)
a__from(
X) →
from(
X)
a__dbl1(
X) →
dbl1(
X)
a__sel1(
X1,
X2) →
sel1(
X1,
X2)
a__quote(
X) →
quote(
X)
Types:
a__dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
0' :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
s :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
nil :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
cons :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
mark :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__from :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
from :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__dbl1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
01' :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
s1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__sel1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__quote :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbl1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
sel1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
quote :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
hole_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote1_0 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0 :: Nat → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
Lemmas:
a__dbl1(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, n3958080_0))) → *3_0, rt ∈ Ω(n39580800)
a__quote(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, n1977765_0))) → *3_0, rt ∈ Ω(n19777650)
Generator Equations:
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(0) ⇔ 0'
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(x, 1)) ⇔ s(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(x))
The following defined symbols remain to be analysed:
a__sel1
They will be analysed ascendingly in the following order:
a__sel = mark
a__sel = a__dbl1
a__sel = a__sel1
a__sel = a__quote
mark = a__dbl1
mark = a__sel1
mark = a__quote
a__dbl1 = a__sel1
a__dbl1 = a__quote
a__sel1 = a__quote
(28) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol a__sel1.
(29) Obligation:
TRS:
Rules:
a__dbl(
0') →
0'a__dbl(
s(
X)) →
s(
s(
dbl(
X)))
a__dbls(
nil) →
nila__dbls(
cons(
X,
Y)) →
cons(
dbl(
X),
dbls(
Y))
a__sel(
0',
cons(
X,
Y)) →
mark(
X)
a__sel(
s(
X),
cons(
Y,
Z)) →
a__sel(
mark(
X),
mark(
Z))
a__indx(
nil,
X) →
nila__indx(
cons(
X,
Y),
Z) →
cons(
sel(
X,
Z),
indx(
Y,
Z))
a__from(
X) →
cons(
X,
from(
s(
X)))
a__dbl1(
0') →
01'a__dbl1(
s(
X)) →
s1(
s1(
a__dbl1(
mark(
X))))
a__sel1(
0',
cons(
X,
Y)) →
mark(
X)
a__sel1(
s(
X),
cons(
Y,
Z)) →
a__sel1(
mark(
X),
mark(
Z))
a__quote(
0') →
01'a__quote(
s(
X)) →
s1(
a__quote(
mark(
X)))
a__quote(
dbl(
X)) →
a__dbl1(
mark(
X))
a__quote(
sel(
X,
Y)) →
a__sel1(
mark(
X),
mark(
Y))
mark(
dbl(
X)) →
a__dbl(
mark(
X))
mark(
dbls(
X)) →
a__dbls(
mark(
X))
mark(
sel(
X1,
X2)) →
a__sel(
mark(
X1),
mark(
X2))
mark(
indx(
X1,
X2)) →
a__indx(
mark(
X1),
X2)
mark(
from(
X)) →
a__from(
X)
mark(
dbl1(
X)) →
a__dbl1(
mark(
X))
mark(
sel1(
X1,
X2)) →
a__sel1(
mark(
X1),
mark(
X2))
mark(
quote(
X)) →
a__quote(
mark(
X))
mark(
0') →
0'mark(
s(
X)) →
s(
X)
mark(
nil) →
nilmark(
cons(
X1,
X2)) →
cons(
X1,
X2)
mark(
01') →
01'mark(
s1(
X)) →
s1(
mark(
X))
a__dbl(
X) →
dbl(
X)
a__dbls(
X) →
dbls(
X)
a__sel(
X1,
X2) →
sel(
X1,
X2)
a__indx(
X1,
X2) →
indx(
X1,
X2)
a__from(
X) →
from(
X)
a__dbl1(
X) →
dbl1(
X)
a__sel1(
X1,
X2) →
sel1(
X1,
X2)
a__quote(
X) →
quote(
X)
Types:
a__dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
0' :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
s :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
nil :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
cons :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
mark :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__from :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
from :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__dbl1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
01' :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
s1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__sel1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__quote :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbl1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
sel1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
quote :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
hole_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote1_0 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0 :: Nat → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
Lemmas:
a__dbl1(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, n3958080_0))) → *3_0, rt ∈ Ω(n39580800)
a__quote(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, n1977765_0))) → *3_0, rt ∈ Ω(n19777650)
Generator Equations:
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(0) ⇔ 0'
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(x, 1)) ⇔ s(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(x))
No more defined symbols left to analyse.
(30) LowerBoundsProof (EQUIVALENT transformation)
The lowerbound Ω(n1) was proven with the following lemma:
a__dbl1(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, n3958080_0))) → *3_0, rt ∈ Ω(n39580800)
(31) BOUNDS(n^1, INF)
(32) Obligation:
TRS:
Rules:
a__dbl(
0') →
0'a__dbl(
s(
X)) →
s(
s(
dbl(
X)))
a__dbls(
nil) →
nila__dbls(
cons(
X,
Y)) →
cons(
dbl(
X),
dbls(
Y))
a__sel(
0',
cons(
X,
Y)) →
mark(
X)
a__sel(
s(
X),
cons(
Y,
Z)) →
a__sel(
mark(
X),
mark(
Z))
a__indx(
nil,
X) →
nila__indx(
cons(
X,
Y),
Z) →
cons(
sel(
X,
Z),
indx(
Y,
Z))
a__from(
X) →
cons(
X,
from(
s(
X)))
a__dbl1(
0') →
01'a__dbl1(
s(
X)) →
s1(
s1(
a__dbl1(
mark(
X))))
a__sel1(
0',
cons(
X,
Y)) →
mark(
X)
a__sel1(
s(
X),
cons(
Y,
Z)) →
a__sel1(
mark(
X),
mark(
Z))
a__quote(
0') →
01'a__quote(
s(
X)) →
s1(
a__quote(
mark(
X)))
a__quote(
dbl(
X)) →
a__dbl1(
mark(
X))
a__quote(
sel(
X,
Y)) →
a__sel1(
mark(
X),
mark(
Y))
mark(
dbl(
X)) →
a__dbl(
mark(
X))
mark(
dbls(
X)) →
a__dbls(
mark(
X))
mark(
sel(
X1,
X2)) →
a__sel(
mark(
X1),
mark(
X2))
mark(
indx(
X1,
X2)) →
a__indx(
mark(
X1),
X2)
mark(
from(
X)) →
a__from(
X)
mark(
dbl1(
X)) →
a__dbl1(
mark(
X))
mark(
sel1(
X1,
X2)) →
a__sel1(
mark(
X1),
mark(
X2))
mark(
quote(
X)) →
a__quote(
mark(
X))
mark(
0') →
0'mark(
s(
X)) →
s(
X)
mark(
nil) →
nilmark(
cons(
X1,
X2)) →
cons(
X1,
X2)
mark(
01') →
01'mark(
s1(
X)) →
s1(
mark(
X))
a__dbl(
X) →
dbl(
X)
a__dbls(
X) →
dbls(
X)
a__sel(
X1,
X2) →
sel(
X1,
X2)
a__indx(
X1,
X2) →
indx(
X1,
X2)
a__from(
X) →
from(
X)
a__dbl1(
X) →
dbl1(
X)
a__sel1(
X1,
X2) →
sel1(
X1,
X2)
a__quote(
X) →
quote(
X)
Types:
a__dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
0' :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
s :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
nil :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
cons :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
mark :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__from :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
from :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__dbl1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
01' :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
s1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__sel1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__quote :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbl1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
sel1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
quote :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
hole_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote1_0 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0 :: Nat → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
Lemmas:
a__dbl1(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, n3958080_0))) → *3_0, rt ∈ Ω(n39580800)
a__quote(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, n1977765_0))) → *3_0, rt ∈ Ω(n19777650)
Generator Equations:
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(0) ⇔ 0'
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(x, 1)) ⇔ s(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(x))
No more defined symbols left to analyse.
(33) LowerBoundsProof (EQUIVALENT transformation)
The lowerbound Ω(n1) was proven with the following lemma:
a__dbl1(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, n3958080_0))) → *3_0, rt ∈ Ω(n39580800)
(34) BOUNDS(n^1, INF)
(35) Obligation:
TRS:
Rules:
a__dbl(
0') →
0'a__dbl(
s(
X)) →
s(
s(
dbl(
X)))
a__dbls(
nil) →
nila__dbls(
cons(
X,
Y)) →
cons(
dbl(
X),
dbls(
Y))
a__sel(
0',
cons(
X,
Y)) →
mark(
X)
a__sel(
s(
X),
cons(
Y,
Z)) →
a__sel(
mark(
X),
mark(
Z))
a__indx(
nil,
X) →
nila__indx(
cons(
X,
Y),
Z) →
cons(
sel(
X,
Z),
indx(
Y,
Z))
a__from(
X) →
cons(
X,
from(
s(
X)))
a__dbl1(
0') →
01'a__dbl1(
s(
X)) →
s1(
s1(
a__dbl1(
mark(
X))))
a__sel1(
0',
cons(
X,
Y)) →
mark(
X)
a__sel1(
s(
X),
cons(
Y,
Z)) →
a__sel1(
mark(
X),
mark(
Z))
a__quote(
0') →
01'a__quote(
s(
X)) →
s1(
a__quote(
mark(
X)))
a__quote(
dbl(
X)) →
a__dbl1(
mark(
X))
a__quote(
sel(
X,
Y)) →
a__sel1(
mark(
X),
mark(
Y))
mark(
dbl(
X)) →
a__dbl(
mark(
X))
mark(
dbls(
X)) →
a__dbls(
mark(
X))
mark(
sel(
X1,
X2)) →
a__sel(
mark(
X1),
mark(
X2))
mark(
indx(
X1,
X2)) →
a__indx(
mark(
X1),
X2)
mark(
from(
X)) →
a__from(
X)
mark(
dbl1(
X)) →
a__dbl1(
mark(
X))
mark(
sel1(
X1,
X2)) →
a__sel1(
mark(
X1),
mark(
X2))
mark(
quote(
X)) →
a__quote(
mark(
X))
mark(
0') →
0'mark(
s(
X)) →
s(
X)
mark(
nil) →
nilmark(
cons(
X1,
X2)) →
cons(
X1,
X2)
mark(
01') →
01'mark(
s1(
X)) →
s1(
mark(
X))
a__dbl(
X) →
dbl(
X)
a__dbls(
X) →
dbls(
X)
a__sel(
X1,
X2) →
sel(
X1,
X2)
a__indx(
X1,
X2) →
indx(
X1,
X2)
a__from(
X) →
from(
X)
a__dbl1(
X) →
dbl1(
X)
a__sel1(
X1,
X2) →
sel1(
X1,
X2)
a__quote(
X) →
quote(
X)
Types:
a__dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
0' :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
s :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
nil :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
cons :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
mark :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__from :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
from :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__dbl1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
01' :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
s1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__sel1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__quote :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbl1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
sel1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
quote :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
hole_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote1_0 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0 :: Nat → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
Lemmas:
a__dbl1(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, n79116_0))) → *3_0, rt ∈ Ω(n791160)
a__quote(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, n1977765_0))) → *3_0, rt ∈ Ω(n19777650)
Generator Equations:
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(0) ⇔ 0'
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(x, 1)) ⇔ s(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(x))
No more defined symbols left to analyse.
(36) LowerBoundsProof (EQUIVALENT transformation)
The lowerbound Ω(n1) was proven with the following lemma:
a__dbl1(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, n79116_0))) → *3_0, rt ∈ Ω(n791160)
(37) BOUNDS(n^1, INF)
(38) Obligation:
TRS:
Rules:
a__dbl(
0') →
0'a__dbl(
s(
X)) →
s(
s(
dbl(
X)))
a__dbls(
nil) →
nila__dbls(
cons(
X,
Y)) →
cons(
dbl(
X),
dbls(
Y))
a__sel(
0',
cons(
X,
Y)) →
mark(
X)
a__sel(
s(
X),
cons(
Y,
Z)) →
a__sel(
mark(
X),
mark(
Z))
a__indx(
nil,
X) →
nila__indx(
cons(
X,
Y),
Z) →
cons(
sel(
X,
Z),
indx(
Y,
Z))
a__from(
X) →
cons(
X,
from(
s(
X)))
a__dbl1(
0') →
01'a__dbl1(
s(
X)) →
s1(
s1(
a__dbl1(
mark(
X))))
a__sel1(
0',
cons(
X,
Y)) →
mark(
X)
a__sel1(
s(
X),
cons(
Y,
Z)) →
a__sel1(
mark(
X),
mark(
Z))
a__quote(
0') →
01'a__quote(
s(
X)) →
s1(
a__quote(
mark(
X)))
a__quote(
dbl(
X)) →
a__dbl1(
mark(
X))
a__quote(
sel(
X,
Y)) →
a__sel1(
mark(
X),
mark(
Y))
mark(
dbl(
X)) →
a__dbl(
mark(
X))
mark(
dbls(
X)) →
a__dbls(
mark(
X))
mark(
sel(
X1,
X2)) →
a__sel(
mark(
X1),
mark(
X2))
mark(
indx(
X1,
X2)) →
a__indx(
mark(
X1),
X2)
mark(
from(
X)) →
a__from(
X)
mark(
dbl1(
X)) →
a__dbl1(
mark(
X))
mark(
sel1(
X1,
X2)) →
a__sel1(
mark(
X1),
mark(
X2))
mark(
quote(
X)) →
a__quote(
mark(
X))
mark(
0') →
0'mark(
s(
X)) →
s(
X)
mark(
nil) →
nilmark(
cons(
X1,
X2)) →
cons(
X1,
X2)
mark(
01') →
01'mark(
s1(
X)) →
s1(
mark(
X))
a__dbl(
X) →
dbl(
X)
a__dbls(
X) →
dbls(
X)
a__sel(
X1,
X2) →
sel(
X1,
X2)
a__indx(
X1,
X2) →
indx(
X1,
X2)
a__from(
X) →
from(
X)
a__dbl1(
X) →
dbl1(
X)
a__sel1(
X1,
X2) →
sel1(
X1,
X2)
a__quote(
X) →
quote(
X)
Types:
a__dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
0' :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
s :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
nil :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
cons :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
mark :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__from :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
from :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__dbl1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
01' :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
s1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__sel1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__quote :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbl1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
sel1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
quote :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
hole_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote1_0 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0 :: Nat → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
Lemmas:
a__dbl1(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, n79116_0))) → *3_0, rt ∈ Ω(n791160)
Generator Equations:
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(0) ⇔ 0'
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(x, 1)) ⇔ s(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(x))
No more defined symbols left to analyse.
(39) LowerBoundsProof (EQUIVALENT transformation)
The lowerbound Ω(n1) was proven with the following lemma:
a__dbl1(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, n79116_0))) → *3_0, rt ∈ Ω(n791160)
(40) BOUNDS(n^1, INF)